Inference at * 1 1 2 
Iof proof for Lemma dcdr-to-bool-equivalence:



1. P : 
2. y : P
3. [inr y ]
  P 

latex

 by ( Unfold `dcdr-to-bool` (-1)) 
CollapseTHEN (Reduce (-1)) 

latex

C1: 

C1: 3. (inr  )
C1:   P
C.

Definitions

[d], b